from z3 import *


# 测试位向量是否是2的幂
def is_power_of_two(x):
    return And(x != 0, 0 == (x & (x - 1)))


x = BitVec("x", 4)
prove(is_power_of_two(x) == Or([x == 2**i for i in range(4)]))

# 获得变量的绝对值
v = BitVec("v", 32)
mask = v >> 31
prove(If(v > 0, v, -v) == (v + mask) ^ mask)


# It declares a floating point number x with 3 bits in the exponent and 4 for the significand.
x = FP("x", FPSort(3, 4))
print(10 + x)
# > 1.25*(2**3) + x
